COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\magnify{1100}
C00016 ENDMK
C⊗;
\magnify{1100}
\def\xskip{\hskip7pt plus3pt minus4pt}
\chcode`|=13
\def|#1|{\hbox{\it#1\/}}
\chcode`⊗=13
\def⊗{\hbox to 2em{}}
\def\IF{\mathop{\bf if}}
\def\THEN{\mathrel{\bf then}}
\def\ELSE{\mathrel{\bf else}}
\def\AND{\mathrel{\bf and}}
\def\OR{\mathrel{\bf or}}
\def\NOT{\mathop{\bf not}}
\def\N{\mathop{\bf n}}
\def\T{\hbox{\tt T}}
\def\NIL{\hbox{\tt NIL}}
\def\.{\mathbin{.}}
\def\A{\mathop{\bf a}}
\def\D{\mathop{\bf d}}
\def\EQ{\mathrel{\bf eq}}
\def\AT{\mathop{\bf at}}
\def\quote#1{\hbox{\sfcode`.=1000\tt#1}}
\def\list#1{\langle#1\rangle}

\ctrline{\bf CS 206---Recursive Programming and Proving}
\vskip 20pt
\ctrline{Writing Proofs}
\ctrline{November 2, 1982}
\vskip 20pt

A number of people have asked about the format in which they should write
their proofs for the homework assignment.  The main question seems to be
how much to say, i.e., what can be assumed without mention, what should be
stated but not proved because it is ``obvious,'' and what level of detail
is required for the things that are proved.

There is no definite answer to these questions, of course, since it is
largely a matter of opinion.  This handout is a set of guidelines that
describes what is desired in a proof, and gives an example similar to the
homework problems.

First, a few words on what does and does not have to be proved.  You can assume
all the rules of first-order logic and arithmetic.  Thus, if you wind up with
$x+0+x=2y$ somewhere, you can immediately reduce this to $x=y$ without an
explanation.  Proofs by induction, however, require mention that this is what
you are doing, and you should identify separately the base case and the
inductive step.  In most of the domains that we are working, there are two
flavors of induction.  For example, with lists we have the axioms
$$\Phi(\NIL)∧(∀u.\,¬\N u∧\Phi(\D u)⊃\Phi(u))⊃(∀u.\,\Phi(u))$$
and
$$\Phi(\NIL)∧(∀x\,u.\,\Phi(u)⊃\Phi(x\.u))⊃(∀u.\,\Phi(u)).$$
You should make it clear which form of induction you are using, and always
identify the predicate $\Phi(u)$ that is being used.

Often you will need to prove a statement that is a subproblem of the main
problem you are working on.  For example, in problem 1.1 on page 89, you may
need to use the fact that $|samelength|[u,v]≡(|length|\,u=|length|\,v)$.
Ask yourself: how obvious is this fact?  Here you may be misled by the fact
that the function is named |samelength|, but that does not mean {\sl a priori\/}
that it actually does what it claims to do.  Many other functions
(|samefringe|, |balanced|, etc.) also have names that suggest their correctness.

The statement $|samelength|[u,v]≡(|length|\,u=|length|\,v)$, then, is something
that has to be proved.  Now you should decide how easy it is to prove.  If it is
a matter of simple transformations and substutions of terms (such as, for
example, $|append|[\NIL,v]=v$) then you can show the substitution in one
line, or, if you are in a hurry, write ``by the definition of |append|,
$\ldotss$.''  However, in the case of the |samelength| function we will need
induction to prove its correctness.  Therefore, it is not trivial, and you
should show all the steps of the induction.

Most of us begin work by attacking the main problem directly and then, when
this requires a lemma to be proved, we either put it off until later or
prove it right away and then continue with the main proof.  Both of these
methods are hard to read, however.  Thus, if you do the proof first as a
rough draft and then recopy it before handing it in, it is best to put
first the proofs of all the lemmas that you are using, and then the main
proof.  Also, please don't turn in parts of your work that turned out to
be ``dead ends'' in an attempted proof.

As an example of these guidelines, consider problem 4.1 on page 89.  The
statement to be proved is $∀x\,u\,v.\,x\in u∪v⊃x\in u∨x\in v$.  The symbols
``$\in$'' and ``$∪$'' are understood to be the |member| function and the
|union| function which is part of problem 22 on page 47.  Below is a proof
that would be suitable as a homework solution.  The proof is given in a
different typeface to separate it from some comments.

\vskip 10pt
{\parskip 8pt \parindent 0pt
\font\ss=cmss10
\def\proof{\leftskip 0.6truein \rightskip 0.6truein\ss}

{\proof
The |member| function is defined on page 16 as
$$|member|[x,u]←\NOT\N u\AND[[x=\A u]\OR|member|[x,\D u]].$$
By the form of the recursion, this function is known to terminate, so
we may use the fact that
$$∀x\,u.\,x\in u≡¬\N u∧(x=\A u∨x\in\D u).$$
\par}
This implicitly uses a lot of the theory developed in chapter 3, but
that's all right.  If we were not sure that |member| terminated, we would
need the techniques in section 3.7.  The reason for starting with this
property of |member| is that we will later discover it is needed as a
lemma, so it is best to get it out of the way before things get
complicated.
\par
{\proof
For the |union| function, which we abbreviate $∪$, we use the program
$$\eqalign{u∪v←\null&\IF\N u\THEN v\cr
&\ELSE\IF \A u\in v\THEN \D u ∪ v\cr
&\ELSE \A u\.[\D u ∪ v].\cr}$$
Let $\Phi(u)$ be the formula $x\in u∪v⊃x\in u∨x\in v$.
\par}
Here you might choose to say, ``We will prove $∀u.\,\Phi(u)$ by induction,''
but it is already fairly clear what you are trying to do.
\par
{\proof First, $\Phi(\NIL)$
is $x\in\NIL∪v⊃x\in\NIL∨x\in v$.  By the definition of $∪$,
$$\eqalign{\NIL∪v&\null=\IF\N\NIL\THEN v\ELSE\ldots\cr
&\null=v,\cr}$$
so the left side of $\Phi(NIL)$ becomes $x\in v$ and $\Phi(\NIL)$ is true.
\par}
Rather than expanding the $∪$, you might have first tried
using the definition
of $\in$ to simplify one of the formulas.  Since this doesn't work, it is left
out of the final proof.
\par
{\proof Now assume $¬\N u$ and $\Phi(\D u)$, which is
$$x\in\D u∪v⊃x\in\D u∨x\in v.$$
From this we will prove $\Phi(u)$.
\par}
It is often useful to write down $\Phi(\D u)$ at this point, as was done, just
so that you can see exactly what it is that you are assuming.  This may help you
decide how to proceed; in this case we will win if we can get
$x\in\D u∪v$ as part of our formula.
\par
{\proof
$$\baselineskip15pt\lineskip3pt\lineskiplimit3pt
\halign{$\displaystyle{#}$&$\displaystyle{#}$\hfill\cr
⊗⊗\Phi(u)&\null≡x\in u∪v⊃x\in u∨x\in v\cr
&\null≡x\in[\IF\A u\in v\THEN\D u∪v\ELSE\A u\.[\D u∪v]]⊃x\in u∨x\in v\cr
\noalign{\hbox{(using the definition of $∪$ and the assumption $¬\N u$)}}
&\null≡|IF|\,\A u\in v\,|THEN|\,x\in\D u∪v⊃x\in u∨x\in v\cr
\noalign{\nobreak}
&⊗|ELSE|\,x\in\A u\.[\D u∪v]⊃x\in u∨x\in v\cr}$$
If $\A u\in v$, we use the inductive assumption to show $x\in\D u∨x\in v$,
and then the definition of $\in$ (above) to show $x\in u∨x\in v$.
In the other case, given $x\in\A u∪v$, the definition of $\in$ can be
used to show that $x=\A u∨x\in\D u∪v$; from the inductive hypothesis this
implies $x=\A u∨x\in\D u∨x\in v$, and, applying the definition of $\in$ one
more time, this proves $x\in u∨x\in v$.
\par}
A lot of details, but each of the steps above is important to show that you
understand why the proof is working.  Some steps were left out, such as
showing that $\A[\A u\.[\D u∪v]]=\A u$ and $\D[\A u\.[\D u∪v]]=\D u∪v$,
because this is fairly straightforward.
\par
{\proof Therefore, $∀u.\,\Phi(u)$ is true.  Since we made no assumptions
about $x$ or $v$, we can quantify over these also and get
$$∀x\,u\,v.\,x\in u∪v⊃x\in u∨x\in v.$$}
\par
} % end this whole business

\vskip 10pt

Notice that there is a lot of text as well as formulas in the proof.  It
helps your proof's readability immensely if you include statements about
the relation of formulas in the proof to each other, especially when you
are referring to facts proved elsewhere.

\vskip 10pt

On an exam, there isn't enough time for a proof as shown above.  You may
be asked only to recognize that induction is needed and to state the
formula $\Phi(u)$ that is used in the induction (or $\Phi(x)$ in the case
of S-expression induction).

If a full proof is asked for, what is expected is that your solution
includes all the necessary steps (thus in an induction, don't leave out
the base case) and include as many of the details as you have time to
write.  If you omit part of a proof, it may seem like you do not know how
to do that part, and you will then not receive credit for it.  Since you
won't have time to recopy your proofs, be sure to cross out any part that
is wrong or does not lead toward the solution.

\vfill\end